$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $a$:$T$, $L$:$T$ List.
\\[0ex]($\forall$$b$:$T$. ($b$ $\in$ insert($a$;$L$)) $\Leftrightarrow$ $b$ $=$ $a$ $\vee$ ($b$ $\in$ $L$))
\\[0ex]\& (no\_repeats($T$;$L$) $\Rightarrow$ no\_repeats($T$;insert($a$;$L$)))